Transformation techniques for context-sensitive rewrite systems
Identifieur interne : 006A45 ( Main/Exploration ); précédent : 006A44; suivant : 006A46Transformation techniques for context-sensitive rewrite systems
Auteurs : Jürgen Giesl [Allemagne] ; Aart Middeldorp [Japon, Allemagne]Source :
- Journal of Functional Programming [ 0956-7968 ] ; 2004-07.
Abstract
Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.
Url:
DOI: 10.1017/S0956796803004945
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001453
- to stream Istex, to step Curation: 001436
- to stream Istex, to step Checkpoint: 001653
- to stream Main, to step Merge: 006D49
- to stream Main, to step Curation: 006A45
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Transformation techniques for context-sensitive rewrite systems</title><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></author><author><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5848583E11137B76FD8915F4719384B061085BBF</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1017/S0956796803004945</idno><idno type="url">https://api.istex.fr/ark:/67375/6GQ-K9HPR2SB-9/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001453</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001453</idno><idno type="wicri:Area/Istex/Curation">001436</idno><idno type="wicri:Area/Istex/Checkpoint">001653</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001653</idno><idno type="wicri:doubleKey">0956-7968:2004:Giesl J:transformation:techniques:for</idno><idno type="wicri:Area/Main/Merge">006D49</idno><idno type="wicri:Area/Main/Curation">006A45</idno><idno type="wicri:Area/Main/Exploration">006A45</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Transformation techniques for context-sensitive rewrite systems</title><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="3"><country wicri:rule="url">Allemagne</country><wicri:regionArea>LuFG Informatik II, RWTH Aachen, Ahornstr. 55, 52074 Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name><affiliation wicri:level="1"><country wicri:rule="url">Japon</country><wicri:regionArea>Institute of Information Sciences and Electronics, University of Tsukuba, Tsukuba 305-8573</wicri:regionArea><wicri:noRegion>Tsukuba 305-8573</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Functional Programming</title><idno type="ISSN">0956-7968</idno><idno type="eISSN">1469-7653</idno><imprint><publisher>Cambridge University Press</publisher><pubPlace>Cambridge, UK</pubPlace><date type="published" when="2004-07">2004-07</date><biblScope unit="volume">14</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="379">379</biblScope><biblScope unit="page" to="427">427</biblScope></imprint><idno type="ISSN">0956-7968</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0956-7968</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract">Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Japon</li></country><region><li>District de Cologne</li><li>Rhénanie-du-Nord-Westphalie</li></region><settlement><li>Aix-la-Chapelle</li></settlement></list><tree><country name="Allemagne"><region name="Rhénanie-du-Nord-Westphalie"><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></region><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name></country><country name="Japon"><noRegion><name sortKey="Middeldorp, Aart" sort="Middeldorp, Aart" uniqKey="Middeldorp A" first="Aart" last="Middeldorp">Aart Middeldorp</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006A45 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006A45 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:5848583E11137B76FD8915F4719384B061085BBF
|texte= Transformation techniques for context-sensitive rewrite systems
}}
| This area was generated with Dilib version V0.6.33. |  |